$\forall$$T$:Type, $R$, $R_{2}$:($T$$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]Refl($T$;$1$,$2$.$R_{2}$($1$,$2$))
\\[0ex]$\Rightarrow$ (Trans $1$,$2$:$T$. $R_{2}$($1$,$2$))
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. ($x$ $R$ $y$) $\Rightarrow$ $R_{2}$($x$,$y$))
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. ($x$ ($R$$^{\mbox{\scriptsize $\ast$}}$) $y$) $\Rightarrow$ $R_{2}$($x$,$y$))